ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
↳ QTRS
↳ DependencyPairsProof
ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
AP2(ap2(ff, x), x) -> AP2(ap2(cons, x), nil)
AP2(ap2(ff, x), x) -> AP2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
AP2(ap2(ff, x), x) -> AP2(x, ap2(ff, x))
AP2(ap2(ff, x), x) -> AP2(cons, x)
ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP2(ap2(ff, x), x) -> AP2(ap2(cons, x), nil)
AP2(ap2(ff, x), x) -> AP2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
AP2(ap2(ff, x), x) -> AP2(x, ap2(ff, x))
AP2(ap2(ff, x), x) -> AP2(cons, x)
ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
AP2(ap2(ff, x), x) -> AP2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
AP2(ap2(ff, x), x) -> AP2(x, ap2(ff, x))
ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP2(ap2(ff, x), x) -> AP2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
AP2(ap2(ff, x), x) -> AP2(x, ap2(ff, x))
POL(AP2(x1, x2)) = x1 + 2·x1·x2
POL(ap2(x1, x2)) = x1 + 2·x1·x2
POL(cons) = 0
POL(ff) = 1
POL(nil) = 0
ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
ap2(ap2(ff, x), x) -> ap2(ap2(x, ap2(ff, x)), ap2(ap2(cons, x), nil))